/*
	・循環参照させない
*/
module filesystem

// オブジェクト
abstract sig Object {}

// ディレクトリ
sig Directory extends Object { 
	contents: set Object
}

// ルートディレクトリ
one sig Root extends Directory{}

// ファイル
sig File extends Object {}

// エイリアス(リンク)
sig Alias extends File {
	to : Object
}

// ファイルは必ずどこかのディレクトリに属する
fact FileBelongsDirectory {
	all f : File | one d: Directory |
		f in d.contents
}

// ルートディレクトリはディレクトリの要素に属さない
fact RootHasNoSuperDir {
	all d: Directory | no r: Root |
		r in d.contents
}

// ディレクトリを循環参照させない
fact NoCycleDir { 
	all d: Directory | no child: d.contents |
		d in child.^contents
}

// 全てのディレクトリ(ルートディレクトリ以外)はルートディレクトリから必ずたどれる
fact DirTraceableRoot {
	one r: Root | all d: Directory - Root |
		d in r.^contents
}

// ルートディレクトリから、ディレクトリへのパスは１つだけ
fact DirTraceableRootOnePath { 
	
}

pred show{}
run show for 7 but 5 Directory
